Nuprl Lemma : chain-consistent-fails-before3 13,45

es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), SysOut:AbsInterface(Top).
(E(Inr E(Sys))
 (f:sys-antecedent(es;Sys).
 (e:E(In). f(e) = e  E)
  (chain:(E(Sys)(Id List)).
  chain-consistent(f;chain)
   (e:E(Sys), i:Id.
   loc(f(e)) << i  i << loc(e cr-fails-before(esSyschaini; loc(f(e)))))) 
latex


Upabstract chain replication
Definitionss = t, t  T, x:AB(x), x:AB(x), ES, EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(Epred?info), kindcase(ka.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,yt(x;y), !Void(), x:A.B(x), Top, S  T, suptype(ST), first(e), A, <ab>, pred(e), x.A(x), xt(x), P & Q, E, AbsInterface(A), e  X, {x:AB(x)} , E(X), sys-antecedent(es;Sys), e c e', let x,y = A in B(x;y), t.1, chain-consistent(f;chain), x:AB(x), P  Q, a < b, hd(l), L1  L2, e loc e' , adjacent(T;L;x;y), (x  l), no_repeats(T;l), Atom$n, loc(e), x << y, x before y  l, cr-fails-before(esSyschainxy), ||as||, #$n, False, , Outcome, A  B, l[i], |g|, A c B, [], [car / cdr], P  Q, P  Q, last(L), (e <loc e'), X(e), if b then t else f fi , {i..j}, increasing(f;k), ff, inr x , tt, inl x , True, case b of inl(x) => s(x) | inr(y) => t(y), f(x)?z, {T}, SQType(T), s ~ t, i  j < k, A List
Lemmasincreasing wf, length wf nat, int seg wf, chain-order-implies-before, before-adjacent, adjacent-member, chain-order transitivity, chain-order-antireflexive, no repeats wf, sublist wf, es-le wf, es-locl wf, adjacent wf, guard wf, Id sq, chain-order-antisymmetric, true wf, btrue wf, bfalse wf, l member subtype, length wf1, select wf, l member wf, false wf, cr-fails-before wf, l before wf, chain-order wf, es-loc wf, chain-consistent wf, es-E-interface-subtype rel, es-causle wf, sys-antecedent wf, es-interface wf, es-E-interface wf, es-is-interface wf, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf

origin